A:Type, I:MaInterface(A), l:IdLnk, tg:Id, nmr:Namer(2;[tg; lname(l)] @ ma-interface-tags(I)).
Normal(A,I)
 gluable(I;l;tg)
 gluable2(A;I;l;tg)
 (k:Knd.
 (k  dom((mapl(i.if i = source(l)
 then ma-interface-conds(I;i)
 else es-in-port-conds(A;(link nmr(0) from i to source(l));nmr(1))
 fi ;remove-repeats(IdDeq;ma-interface-locs(I))))))
  (hasloc(k;source(l)))) 

latex

Definitions

x:A. B(x), P  Q, t  T, , A  B, A, False, (x  l), a:A fp B(a), Knd, if b then t else f fi , , x. t(x), x:A. B(x), A c B, tt, ff, Top, SQType(T), {T}, P & Q, {i..j}, i  j < k, (link n from i to j), rcv(l,tg), b, isrcv(k), destination(l), lnk(k), isl(x), t.1, t.2, outl(x), Namer(n;Id_list), , x(s), Unit, P  Q, (xL.P(x)), P  Q, ma-interface-conds(I;i), fpf-domain(f), es-in-port-conds(A;l;tg), P  Q, , a = b

Lemmas

interfaceGlue helper0, gluable2 wf, gluable wf, ma-interface-normal wf, Namer wf, le wf, append wf, Id wf, lname wf, ma-interface-tags wf, IdLnk wf, ma-interface wf, Knd wf, assert wf, fpf-dom wf, fpf-join-list wf, top wf, mapl wf, l member wf, nat wf, length wf1, select wf, eq id wf, lsrc wf, bool wf, iff transitivity, eqtt to assert, assert-eq-id, ma-interface-conds wf, member-remove-repeats, fpf-trivial-subtype-top, decl-state wf, ma-interface-ds wf, fpf wf, bnot wf, not wf, eqff to assert, assert of bnot, not functionality wrt iff, es-in-port-conds wf, mk lnk wf, fpf-join-list-dom2, assert-ma-interface-loc, ma-interface-loc wf, fpf-empty wf, subtype rel list, subtype-fpf2, member-mapl, bool cases, bool sq, Id sq, member-fpf-domain, ma-interface-dom-hasloc, Kind-deq wf, fpf-single-dom-sq, rcv wf, assert-eq-knd, Knd sq, assert-hasloc, true wf